Section: Contracts and Grants with Industry

Diagnosis of errors in network controlled systems

Participants : Diego Caminha Barbosa de Oliveira, Pascal Fontaine, Stephan Merz.

In an exploratory project with Westinghouse France, we studied the possibility of using formal verification technology (in particular model checking and SAT/SMT solving) for diagnosing possibly transient faults in communication networks. The diagnosis is based on logs that are generated by periodic self tests. In particular, the SAT solver of veriT has been interfaced with Matlab so that it can be used by our industrial partner for determining causes of certain permanent faults. We have also used Uppaal to model a simplified version of a protocol used by our industrial partner in order to determine timing intervals for the occurrence of faults detected in logs.